1 /-
2 Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Sébastien Gouëzel
5 -/
6
7 import geometry.manifold.smooth_manifold_with_corners linear_algebra.finite_dimensional
src └────────────────────────────────────────────┘ └───────────────────────────────┘
8
9 /-!
10 # Constructing examples of manifolds over ℝ
11
12 We introduce the necessary bits to be able to define manifolds modelled over ℝ^n, boundaryless
13 or with boundary or with corners. As a concrete example, we construct explicitly the manifold with
14 boundary structure on the real interval [x, y].
15
16 More specifically, we introduce
17 * `euclidean_space n` for a model vector space of dimension `n`.
18 * `model_with_corners ℝ (euclidean_space n) (euclidean_half_space n)` for the model space used
19 to define `n`-dimensional real manifolds with boundary
20 * `model_with_corners ℝ (euclidean_space n) (euclidean_quadrant n)` for the model space used
21 to define `n`-dimensional real manifolds with corners
22
23 ## Implementation notes
24
25 The manifold structure on the interval [x, y] = Icc x y requires the assumption `x < y`. We
26 introduce a dummy class `lt_class x y` for this, to make such an assumption available to typeclass
27 search. This should hopefully not be necessary any more in Lean 4.
28 -/
29
30 noncomputable theory
31 open set
32
33 /--
34 The space ℝ^n. Note that the name is slightly misleading, as we only need a normed space
35 structure on ℝ^n, but the one we use here is the sup norm and not the euclidean one -- this is not
36 a problem for the manifold applications, but should probably be refactored at some point.
37 -/
38 def euclidean_space (n : ℕ) : Type := (fin n → ℝ)
id ┴ └─┘ ┴ ┴
src ┴ └─┘ ┴
typ ┴ └─┘ ┴ ┴
39
40 /--
41 The half-space in ℝ^n, used to model manifolds with boundary. We only define it when `1 ≤ n`, as the
42 definition only makes sense in this case.
43 -/
44 def euclidean_half_space (n : ℕ) [has_zero (fin n)] : Type :=
id ┴ └──────┘ └─┘ ┴
src ┴ └──────┘ └─┘
typ ┴ └──────┘ └─┘ ┴
45 {x : euclidean_space n // 0 ≤ x 0}
id ┴ └─────────────┘ ┴ ┴ ┴
src ┴ └─────────────┘ ┴
typ ┴ └─────────────┘ ┴ ┴ ┴
doc └─────────────┘
46
47 /--
48 The quadrant in ℝ^n, used to model manifolds with corners, made of all vectors with nonnegative
49 coordinates.
50 -/
51 def euclidean_quadrant (n : ℕ) : Type := {x : euclidean_space n // ∀i:fin n, 0 ≤ x i}
id ┴ ┴ └─────────────┘ ┴ └─┘ ┴ ┴ ┴ ┴
src ┴ ┴ └─────────────┘ └─┘ ┴
typ ┴ ┴ └─────────────┘ ┴ └─┘ ┴ ┴ ┴ ┴
doc └─────────────┘
52
53 section
54 /- Register class instances for euclidean space and half-space and quadrant -/
55 local attribute [reducible] euclidean_space euclidean_half_space euclidean_quadrant
id └─────────────┘ └──────────────────┘ └────────────────┘
src └─────────────┘ └──────────────────┘ └────────────────┘
typ └─────────────┘ └──────────────────┘ └────────────────┘
doc └───────┘ └─────────────┘ └──────────────────┘ └────────────────┘
56 variable {n : ℕ}
id ┴
src ┴
typ ┴
57
58 -- short-circuit type class inference
59 instance : vector_space ℝ (euclidean_space n) := by apply_instance
id └──────────┘ ┴ └─────────────┘ ┴
src └──────────┘ ┴ └─────────────┘ └─────────────┘
typ └──────────┘ ┴ └─────────────┘ ┴ └─────────────┘
doc └──────────┘ └─────────────┘ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
60 instance : normed_group (euclidean_space n) := by apply_instance
id └──────────┘ └─────────────┘ ┴
src └──────────┘ └─────────────┘ └─────────────┘
typ └──────────┘ └─────────────┘ ┴ └─────────────┘
doc └──────────┘ └─────────────┘ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
61 instance : normed_space ℝ (euclidean_space n) := by apply_instance
id └──────────┘ ┴ └─────────────┘ ┴
src └──────────┘ ┴ └─────────────┘ └─────────────┘
typ └──────────┘ ┴ └─────────────┘ ┴ └─────────────┘
doc └──────────┘ └─────────────┘ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
62 instance [has_zero (fin n)] : topological_space (euclidean_half_space n) := by apply_instance
id └──────┘ └─┘ ┴ └───────────────┘ └──────────────────┘ ┴
src └──────┘ └─┘ └───────────────┘ └──────────────────┘ └─────────────┘
typ └──────┘ └─┘ ┴ └───────────────┘ └──────────────────┘ ┴ └─────────────┘
doc └───────────────┘ └──────────────────┘ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
63 instance : topological_space (euclidean_quadrant n) := by apply_instance
id └───────────────┘ └────────────────┘ ┴
src └───────────────┘ └────────────────┘ └─────────────┘
typ └───────────────┘ └────────────────┘ ┴ └─────────────┘
doc └───────────────┘ └────────────────┘ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
64 instance : finite_dimensional ℝ (euclidean_space n) := by apply_instance
id └────────────────┘ ┴ └─────────────┘ ┴
src └────────────────┘ ┴ └─────────────┘ └──────────────
typ └────────────────┘ ┴ └─────────────┘ ┴ └──────────────
doc └────────────────┘ └─────────────┘ └──────────────
txt └──────────────
par └──────────────
pid └
st └───────────────
65
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
66 @[simp] lemma findim_euclidean_space : finite_dimensional.findim ℝ (euclidean_space n) = n :=
id └───────────────────────┘ ┴ └─────────────┘ ┴ ┴ ┴
src └───────────────────────┘ ┴ └─────────────┘ ┴
typ └───────────────────────┘ ┴ └─────────────┘ ┴ ┴ ┴
doc └──┘ └───────────────────────┘ └─────────────┘
67 by simp
src └────
typ └────
doc └────
txt └────
par └────
pid └
68
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
69 lemma range_half_space (n : ℕ) [has_zero (fin n)] :
70 range (λx : euclidean_half_space n, x.val) = {y | 0 ≤ y 0 } :=
71 by simp
src └────
typ └────
doc └────
txt └────
par └────
pid └
72
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
73 lemma range_quadrant (n : ℕ) :
74 range (λx : euclidean_quadrant n, x.val) = {y | ∀i:fin n, 0 ≤ y i } :=
75 by simp
src └────
typ └────
doc └────
txt └────
par └────
pid └
76
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
77 end
78
79 /--
80 Definition of the model with corners (euclidean_space n, euclidean_half_space n), used as a
81 model for manifolds with boundary.
82 -/
83 def model_with_corners_euclidean_half_space (n : ℕ) [has_zero (fin n)] :
84 model_with_corners ℝ (euclidean_space n) (euclidean_half_space n) :=
85 { to_fun := λx, x.val,
86 inv_fun := λx, ⟨λi, if h : i = 0 then max (x i) 0 else x i, by simp [le_refl]⟩,
src └────┘ ┴
typ └────┘ ┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
87 source := univ,
88 target := range (λx : euclidean_half_space n, x.val),
89 map_source := λx hx, by simpa [-mem_range, mem_range_self] using x.property,
src └─────────────────┘ └──────┘
typ └─────────────────┘ └──────┘
doc └─────────────────┘ └──────┘
txt └─────────────────┘ └──────┘
par └─────────────────┘ └──────┘
pid ┴└───────────┘ ┴┴└────┘
90 map_target := λx hx, mem_univ _,
91 left_inv := λ⟨xval, xprop⟩ hx, begin
92 rw subtype.mk_eq_mk,
id └──────────────┘
src └─┘└──────────────┘
typ └─┘└──────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st └────────────────┘└─
93 ext1 i,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid └┘
st ─────────┘└─
94 by_cases hi : i = 0;
id ┴ ┴
src └───────┘ └─┘ ┴┴└┘
typ └───────┘ └─┘┴┴┴└┘
doc └───────┘ └─┘ ┴ └┘
txt └───────┘ └─┘ ┴ └┘
par └───────┘ └─┘ ┴ └┘
pid ┴ └─┘ ┴ ┴┴
st ─────────────────────────
95 simp [hi, xprop]
id └┘ └───┘
src └────┘ └┘ └─
typ └────┘└┘└┘└───┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st ─────────────────────
96 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
97 right_inv := λx hx, begin
id ┴ └┘
typ ┴ └┘
st └─────
98 simp [range_half_space] at hx,
id └──────────────┘
src └────┘└──────────────┘└─────┘
typ └────┘└──────────────┘└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴┴ ┴┴└───┘
st ────────────────────────────────┘└─
99 ext1 i,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid └┘
st ─────────┘└─
100 by_cases hi : i = 0;
id ┴
src └───────┘ └─┘ ┴ └┘
typ └───────┘ └─┘┴┴ └┘
doc └───────┘ └─┘ ┴ └┘
txt └───────┘ └─┘ ┴ └┘
par └───────┘ └─┘ ┴ └┘
pid ┴ └─┘ ┴ ┴┴
st ─────────────────────────
101 simp [hi, hx]
id └┘ └┘
src └────┘ └┘ └─
typ └────┘└┘└┘└┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st ──────────────────
102 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
103 source_eq := rfl,
id └─┘
src └─┘
typ └─┘
104 unique_diff := begin
st └─────
105 /- To check that the half-space has the unique differentiability property, we use the criterion
st ────────────────────────────────────────────────────────────────────────────────────────────────────
106 `unique_diff_on_convex`: it suffices to check that it is convex and with nonempty interior. -/
st ───────────────────────────────────────────────────────────────────────────────────────────────────
107 rw range_half_space,
id └──────────────┘
src └─┘└──────────────┘
typ └─┘└──────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────────────────┘└─
108 apply unique_diff_on_convex,
id └───────────────────┘
src └────┘└───────────────────┘
typ └────┘└───────────────────┘
doc └────┘└───────────────────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────────────┘└─
109 show convex {y : euclidean_space n | 0 ≤ y 0},
id └────┘ ┴ └─────────────┘ ┴ ┴
src └───┘└────┘┴┴└──┘└─────────────┘┴ └───┘┴┴ └─┘
typ └───┘└────┘┴┴└──┘└─────────────┘┴┴└───┘┴┴ └─┘
doc └───┘└────┘┴ └──┘└─────────────┘┴ └───┘ ┴ └─┘
txt └───┘ ┴ └──┘ ┴ └───┘ ┴ └─┘
par └───┘ ┴ └──┘ ┴ └───┘ ┴ └─┘
pid └───┘ ┴ └──┘ ┴ └───┘ ┴ └─┘
st ────────────────────────────────────────────────┘└─
110 { assume x y hx hy a b ha hb hab,
src └────────────────────────────┘
typ └────────────────────────────┘
doc └────────────────────────────┘
txt └────────────────────────────┘
par └────────────────────────────┘
pid └────────────────────────────┘
st ─────┘└────────────────────────────┘└─
111 simpa using add_le_add (mul_nonneg' ha hx) (mul_nonneg' hb hy) },
id └────────┘ └┘ └┘ └─────────┘ └┘ └┘
src └──────────┘└────────┘┴ ┴ ┴ └┘ └─────────┘┴ ┴ └┘
typ └──────────┘└────────┘┴ ┴└┘┴└┘└┘ └─────────┘┴└┘┴└┘└┘
doc └──────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘
txt └──────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘
par └──────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘
pid ┴└────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴┴
st ────────────────────────────────────────────────────────────────────┘└┘└
112 show (interior {y : euclidean_space n | 0 ≤ y 0}).nonempty,
id └──────┘ ┴ └─────────────┘ ┴
src └───┘ └──────┘┴┴└──┘└─────────────┘┴ └───┘ ┴ └───────────┘
typ └───┘ └──────┘┴┴└──┘└─────────────┘┴┴└───┘ ┴ └───────────┘
doc └───┘ └──────┘┴ └──┘└─────────────┘┴ └───┘ ┴ └───────────┘
txt └───┘ ┴ └──┘ ┴ └───┘ ┴ └───────────┘
par └───┘ ┴ └──┘ ┴ └───┘ ┴ └───────────┘
pid └───┘ ┴ └──┘ ┴ └───┘ ┴ └──────────┘┴
st ────────────────────────────────────────────────────────────────
113 { use (λi, 1),
src └──┘ └───┘
typ └──┘ └───┘
doc └──┘ └───┘
txt └──┘ └───┘
par └──┘ └───┘
pid ┴ └───┘
st ────────────────┘└─
114 rw mem_interior,
id └──────────┘
src └─┘└──────────┘
typ └─┘└──────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────────────┘└─
115 refine ⟨(pi (univ : set (fin n)) (λi, (Ioi 0 : set ℝ))), _,
id └┘ └──┘ └─┘ ┴ └─┘ └─┘
src └─────┘ └┘┴ └──┘└─┘ ┴ └─┘┴ └─┘ └─┘ └─┘└───┘└─┘┴ └───────
typ └─────┘ └┘┴ └──┘└─┘ ┴ └─┘┴┴└─┘ └─┘ └─┘└───┘└─┘┴ └───────
doc └─────┘ └┘┴ └─┘ ┴ ┴ └─┘ └─┘ └─┘└───┘ ┴ └───────
txt └─────┘ ┴ └─┘ ┴ ┴ └─┘ └─┘ └───┘ ┴ └───────
par └─────┘ ┴ └─┘ ┴ ┴ └─┘ └─┘ └───┘ ┴ └───────
pid ┴ ┴ └─┘ ┴ ┴ └─┘ └─┘ └───┘ ┴ └───────
st ──────────────────────────────────────────────────────────────────
116 is_open_set_pi finite_univ (λa ha, is_open_Ioi), _⟩,
id └────────────┘ └─────────┘ └─────────┘
src ───────┘└────────────┘┴└─────────┘┴ └────┘└─────────┘└───┘
typ ───────┘└────────────┘┴└─────────┘┴ └────┘└─────────┘└───┘
doc ───────┘ ┴ ┴ └────┘ └───┘
txt ───────┘ ┴ ┴ └────┘ └───┘
par ───────┘ ┴ ┴ └────┘ └───┘
pid ───────┘ ┴ ┴ └────┘ └───┘
st ──────────────────────────────────────────────────────────┘└─
117 { assume x hx,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ───────┘└─────────┘└─
118 simp [pi] at hx,
id └┘
src └────┘└┘└─────┘
typ └────┘└┘└─────┘
doc └────┘└┘└─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴┴ ┴┴└───┘
st ──────────────────────┘└─
119 exact le_of_lt (hx 0) },
id └──────┘ └┘
src └────┘└──────┘┴ └──┘
typ └────┘└──────┘┴ └┘└──┘
doc └────┘ ┴ └──┘
txt └────┘ ┴ └──┘
par └────┘ ┴ └──┘
pid ┴ ┴ └─┘┴
st ─────────────────────────────┘└┘└
120 { simp only [pi, forall_prop_of_true, mem_univ, mem_Ioi],
id └┘ └─────────────────┘ └──────┘ └─────┘
src └─────────┘└┘└┘└─────────────────┘└┘└──────┘└┘└─────┘┴
typ └─────────┘└┘└┘└─────────────────┘└┘└──────┘└┘└─────┘┴
doc └─────────┘└┘└┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ ┴
st ─────────────────────────────────────────────────────────────┘└─
121 assume i,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───────────────┘└─
122 exact zero_lt_one } }
id └─────────┘
src └────┘└─────────┘┴
typ └────┘└─────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────────────┘└───
123 end,
st ────┘
124 continuous_to_fun := continuous_subtype_val,
id └────────────────────┘
src └────────────────────┘
typ └────────────────────┘
125 continuous_inv_fun := begin
st └─────
126 apply continuous_subtype_mk,
id └───────────────────┘
src └────┘└───────────────────┘
typ └────┘└───────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────────────┘└─
127 apply continuous_pi,
id └───────────┘
src └────┘└───────────┘
typ └────┘└───────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────┘└─
128 assume i,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───────────┘└─
129 by_cases h : i = 0,
id ┴
src └───────┘ └─┘ ┴ └┘
typ └───────┘ └─┘┴┴ └┘
doc └───────┘ └─┘ ┴ └┘
txt └───────┘ └─┘ ┴ └┘
par └───────┘ └─┘ ┴ └┘
pid ┴ └─┘ ┴ ┴┴
st ─────────────────────┘└─
130 { simp only [h, dif_pos],
id ┴ └─────┘
src └─────────┘ └┘└─────┘┴
typ └─────────┘┴└┘└─────┘┴
doc └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st ─────┘└────────────────────┘└─
131 have : continuous (λx:ℝ, max x 0) := continuous_id.max continuous_const,
id └────────┘ └─┘ └───────────────┘ └──────────────┘
src └─────┘└────────┘┴ └┘ └┘└─┘┴ └─────┘└───────────────┘┴└──────────────┘
typ └─────┘└────────┘┴ └┘ └┘└─┘┴ └─────┘└───────────────┘┴└──────────────┘
doc └─────┘└────────┘┴ └┘ └┘ ┴ └─────┘ ┴
txt └─────┘ ┴ └┘ └┘ ┴ └─────┘ ┴
par └─────┘ ┴ └┘ └┘ ┴ └─────┘ ┴
pid └───┘└┘ ┴ └┘ └┘ ┴ └─┘└──┘ ┴
st ────────────────────────────────────────────────────────────────────────────┘└─
132 exact this.comp (continuous_apply 0) },
id └───────┘ └──────────────┘
src └────┘└───────┘┴ └──────────────┘└──┘
typ └────┘└───────┘┴ └──────────────┘└──┘
doc └────┘ ┴ └──┘
txt └────┘ ┴ └──┘
par └────┘ ┴ └──┘
pid ┴ ┴ └─┘┴
st ──────────────────────────────────────────┘└┘└
133 { simp [h],
id ┴
src └────┘ ┴
typ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ─────────────┘└─
134 exact continuous_apply i }
id └──────────────┘ ┴
src └────┘└──────────────┘┴ ┴
typ └────┘└──────────────┘┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ──────────────────────────────┘└─
135 end }
st ────┘
136
137 /--
138 Definition of the model with corners (euclidean_space n, euclidean_quadrant n), used as a
139 model for manifolds with corners -/
140 def model_with_corners_euclidean_quadrant (n : ℕ) :
id ┴
src ┴
typ ┴
141 model_with_corners ℝ (euclidean_space n) (euclidean_quadrant n) :=
id └────────────────┘ ┴ └─────────────┘ ┴ └────────────────┘ ┴
src └────────────────┘ ┴ └─────────────┘ └────────────────┘
typ └────────────────┘ ┴ └─────────────┘ ┴ └────────────────┘ ┴
doc └────────────────┘ └─────────────┘ └────────────────┘
142 { to_fun := λx, x.val,
id ┴ ┴└──┘
src └──┘
typ ┴ ┴└──┘
143 inv_fun := λx, ⟨λi, max (x i) 0,
id ┴ ┴ └─┘ ┴ ┴
src └─┘
typ ┴ ┴ └─┘ ┴ ┴
144 λi, by simp [le_refl]⟩,
id ┴ └─────┘
src └────┘└─────┘┴
typ ┴ └────┘└─────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └─────────────┘
145 source := univ,
id └──┘
src └──┘
typ └──┘
146 target := range (λx : euclidean_quadrant n, x.val),
id └───┘ └────────────────┘ ┴ ┴└──┘
src └───┘ └────────────────┘ └──┘
typ └───┘ └────────────────┘ ┴ ┴└──┘
doc └───┘ └────────────────┘
147 map_source := λx hx, by simpa [-mem_range, mem_range_self] using x.property,
id ┴ └┘ └────────────┘ └────────┘
src └─────────────────┘└────────────┘└──────┘└────────┘
typ ┴ └┘ └─────────────────┘└────────────┘└──────┘└────────┘
doc └─────────────────┘ └──────┘
txt └─────────────────┘ └──────┘
par └─────────────────┘ └──────┘
pid ┴└───────────┘ ┴┴└────┘
st └──────────────────────────────────────────────────┘
148 map_target := λx hx, mem_univ _,
id ┴ └┘ └──────┘
src └──────┘
typ ┴ └┘ └──────┘
149 left_inv := λ⟨xval, xprop⟩ hx, begin
id ┴ └┘
typ ┴ └┘
st └─────
150 rw subtype.mk_eq_mk,
id └──────────────┘
src └─┘└──────────────┘
typ └─┘└──────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────────────────┘└─
151 ext1 i,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid └┘
st ─────────┘└─
152 simp [xprop i]
id └───┘ ┴
src └────┘ ┴ └─
typ └────┘└───┘┴┴└─
doc └────┘ ┴ └─
txt └────┘ ┴ └─
par └────┘ ┴ └─
pid ┴┴ ┴ ┴└
st ───────────────────
153 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
154 right_inv := λx hx, begin
id ┴ └┘
typ ┴ └┘
st └─────
155 rw range_quadrant at hx,
id └────────────┘
src └─┘└────────────┘└────┘
typ └─┘└────────────┘└────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ └────┘
st ──────────────────────────┘└─
156 ext1 i,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid └┘
st ─────────┘└─
157 simp [hx i]
id └┘ ┴
src └────┘ ┴ └─
typ └────┘└┘┴┴└─
doc └────┘ ┴ └─
txt └────┘ ┴ └─
par └────┘ ┴ └─
pid ┴┴ ┴ ┴└
st ────────────────
158 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
159 source_eq := rfl,
id └─┘
src └─┘
typ └─┘
160 unique_diff := begin
st └─────
161 /- To check that the quadrant has the unique differentiability property, we use the criterion
st ──────────────────────────────────────────────────────────────────────────────────────────────────
162 `unique_diff_on_convex`: it suffices to check that it is convex and with nonempty interior. -/
st ───────────────────────────────────────────────────────────────────────────────────────────────────
163 rw range_quadrant,
id └────────────┘
src └─┘└────────────┘
typ └─┘└────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────────────┘└─
164 apply unique_diff_on_convex,
id └───────────────────┘
src └────┘└───────────────────┘
typ └────┘└───────────────────┘
doc └────┘└───────────────────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────────────┘└─
165 show convex {y : euclidean_space n | ∀ (i : fin n), 0 ≤ y i},
id └────┘ ┴ └─────────────┘ └─┘ ┴ ┴
src └───┘└────┘┴┴└──┘└─────────────┘┴ └─┘ └────┘└─┘┴ ┴ └─┘┴┴ ┴ ┴
typ └───┘└────┘┴┴└──┘└─────────────┘┴ └─┘ └────┘└─┘┴┴┴ └─┘┴┴ ┴ ┴
doc └───┘└────┘┴ └──┘└─────────────┘┴ └─┘ └────┘ ┴ ┴ └─┘ ┴ ┴ ┴
txt └───┘ ┴ └──┘ ┴ └─┘ └────┘ ┴ ┴ └─┘ ┴ ┴ ┴
par └───┘ ┴ └──┘ ┴ └─┘ └────┘ ┴ ┴ └─┘ ┴ ┴ ┴
pid └───┘ ┴ └──┘ ┴ └─┘ └────┘ ┴ ┴ └─┘ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────┘└─
166 { assume x y hx hy a b ha hb hab i,
src └──────────────────────────────┘
typ └──────────────────────────────┘
doc └──────────────────────────────┘
txt └──────────────────────────────┘
par └──────────────────────────────┘
pid └──────────────────────────────┘
st ─────┘└──────────────────────────────┘└─
167 simpa using add_le_add (mul_nonneg' ha (hx i)) (mul_nonneg' hb (hy i)) },
id └────────┘ └┘ └┘ └─────────┘ └┘ └┘ ┴
src └──────────┘└────────┘┴ ┴ ┴ ┴ └─┘ └─────────┘┴ ┴ ┴ └─┘
typ └──────────┘└────────┘┴ ┴└┘┴ └┘┴ └─┘ └─────────┘┴└┘┴ └┘┴┴└─┘
doc └──────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘
txt └──────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘
par └──────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘
pid ┴└────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘┴
st ────────────────────────────────────────────────────────────────────────────┘└┘└
168 show (interior {y : euclidean_space n | ∀ (i : fin n), 0 ≤ y i}).nonempty,
id └──────┘ ┴ └─────────────┘ └─┘ ┴
src └───┘ └──────┘┴┴└──┘└─────────────┘┴ └─┘ └────┘└─┘┴ ┴ └─┘ ┴ ┴ └─────────┘
typ └───┘ └──────┘┴┴└──┘└─────────────┘┴ └─┘ └────┘└─┘┴┴┴ └─┘ ┴ ┴ └─────────┘
doc └───┘ └──────┘┴ └──┘└─────────────┘┴ └─┘ └────┘ ┴ ┴ └─┘ ┴ ┴ └─────────┘
txt └───┘ ┴ └──┘ ┴ └─┘ └────┘ ┴ ┴ └─┘ ┴ ┴ └─────────┘
par └───┘ ┴ └──┘ ┴ └─┘ └────┘ ┴ ┴ └─┘ ┴ ┴ └─────────┘
pid └───┘ ┴ └──┘ ┴ └─┘ └────┘ ┴ ┴ └─┘ ┴ ┴ └────────┘┴
st ───────────────────────────────────────────────────────────────────────────────
169 { use (λi, 1),
src └──┘ └───┘
typ └──┘ └───┘
doc └──┘ └───┘
txt └──┘ └───┘
par └──┘ └───┘
pid ┴ └───┘
st ────────────────┘└─
170 rw mem_interior,
id └──────────┘
src └─┘└──────────┘
typ └─┘└──────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────────────┘└─
171 refine ⟨(pi (univ : set (fin n)) (λi, (Ioi 0 : set ℝ))), _,
id └┘ └──┘ └─┘ ┴ └─┘ └─┘
src └─────┘ └┘┴ └──┘└─┘ ┴ └─┘┴ └─┘ └─┘ └─┘└───┘└─┘┴ └───────
typ └─────┘ └┘┴ └──┘└─┘ ┴ └─┘┴┴└─┘ └─┘ └─┘└───┘└─┘┴ └───────
doc └─────┘ └┘┴ └─┘ ┴ ┴ └─┘ └─┘ └─┘└───┘ ┴ └───────
txt └─────┘ ┴ └─┘ ┴ ┴ └─┘ └─┘ └───┘ ┴ └───────
par └─────┘ ┴ └─┘ ┴ ┴ └─┘ └─┘ └───┘ ┴ └───────
pid ┴ ┴ └─┘ ┴ ┴ └─┘ └─┘ └───┘ ┴ └───────
st ──────────────────────────────────────────────────────────────────
172 is_open_set_pi finite_univ (λa ha, is_open_Ioi), _⟩,
id └────────────┘ └─────────┘ └─────────┘
src ───────┘└────────────┘┴└─────────┘┴ └────┘└─────────┘└───┘
typ ───────┘└────────────┘┴└─────────┘┴ └────┘└─────────┘└───┘
doc ───────┘ ┴ ┴ └────┘ └───┘
txt ───────┘ ┴ ┴ └────┘ └───┘
par ───────┘ ┴ ┴ └────┘ └───┘
pid ───────┘ ┴ ┴ └────┘ └───┘
st ──────────────────────────────────────────────────────────┘└─
173 { assume x hx i,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └───────────┘
st ───────┘└───────────┘└─
174 simp [pi] at hx,
id └┘
src └────┘└┘└─────┘
typ └────┘└┘└─────┘
doc └────┘└┘└─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴┴ ┴┴└───┘
st ──────────────────────┘└─
175 exact le_of_lt (hx i) },
id └──────┘ └┘ ┴
src └────┘└──────┘┴ ┴ └┘
typ └────┘└──────┘┴ └┘┴┴└┘
doc └────┘ ┴ ┴ └┘
txt └────┘ ┴ ┴ └┘
par └────┘ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴┴
st ─────────────────────────────┘└┘└
176 { simp only [pi, forall_prop_of_true, mem_univ, mem_Ioi],
id └┘ └─────────────────┘ └──────┘ └─────┘
src └─────────┘└┘└┘└─────────────────┘└┘└──────┘└┘└─────┘┴
typ └─────────┘└┘└┘└─────────────────┘└┘└──────┘└┘└─────┘┴
doc └─────────┘└┘└┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ ┴
st ─────────────────────────────────────────────────────────────┘└─
177 assume i,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───────────────┘└─
178 exact zero_lt_one } }
id └─────────┘
src └────┘└─────────┘┴
typ └────┘└─────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────────────┘└───
179 end,
st ────┘
180 continuous_to_fun := continuous_subtype_val,
id └────────────────────┘
src └────────────────────┘
typ └────────────────────┘
181 continuous_inv_fun := begin
st └─────
182 apply continuous_subtype_mk,
id └───────────────────┘
src └────┘└───────────────────┘
typ └────┘└───────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────────────┘└─
183 apply continuous_pi,
id └───────────┘
src └────┘└───────────┘
typ └────┘└───────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────┘└─
184 assume i,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───────────┘└─
185 have : continuous (λx:ℝ, max x 0) := continuous.max continuous_id continuous_const,
id └────────┘ └─┘ └────────────┘ └───────────┘ └──────────────┘
src └─────┘└────────┘┴ └┘ └┘└─┘┴ └─────┘└────────────┘┴└───────────┘┴└──────────────┘
typ └─────┘└────────┘┴ └┘ └┘└─┘┴ └─────┘└────────────┘┴└───────────┘┴└──────────────┘
doc └─────┘└────────┘┴ └┘ └┘ ┴ └─────┘ ┴ ┴
txt └─────┘ ┴ └┘ └┘ ┴ └─────┘ ┴ ┴
par └─────┘ ┴ └┘ └┘ ┴ └─────┘ ┴ ┴
pid └───┘└┘ ┴ └┘ └┘ ┴ └─┘└──┘ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────────────────┘└─
186 exact this.comp (continuous_apply i)
id └───────┘ └──────────────┘ ┴
src └────┘└───────┘┴ └──────────────┘┴ └─
typ └────┘└───────┘┴ └──────────────┘┴┴└─
doc └────┘ ┴ ┴ └─
txt └────┘ ┴ ┴ └─
par └────┘ ┴ ┴ └─
pid ┴ ┴ ┴ ┴└
st ─────────────────────────────────────────
187 end }
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
188
189 /--
190 Dummy class to make an assumption such as `x < y` available to typeclass search. Such an
191 assumption is used to define a manifold structure on [x, y] when `x < y`. Should be fixed in Lean 4.
192 -/
193 def lt_class {α : Type*} [has_lt α] (x y : α) : Prop := x < y
id └────┘ ┴ ┴ ┴ ┴ ┴
src └────┘ ┴
typ └────┘ ┴ ┴ ┴ ┴ ┴
194 attribute [class] lt_class
id └──────┘
src └──────┘
typ └──────┘
doc └──────┘
195
196 /--
197 The left chart for the topological space [x, y], defined on [x,y) and sending x to 0 in
198 `euclidean_half_space 1`.
199 -/
200 def Icc_left_chart (x y : ℝ) [h : lt_class x y] :
id ┴ └──────┘ ┴ ┴
src ┴ └──────┘
typ ┴ └──────┘ ┴ ┴
doc └──────┘
201 local_homeomorph (Icc x y) (euclidean_half_space 1) :=
id └──────────────┘ └─┘ ┴ ┴ └──────────────────┘
src └──────────────┘ └─┘ └──────────────────┘
typ └──────────────┘ └─┘ ┴ ┴ └──────────────────┘
doc └──────────────┘ └─┘ └──────────────────┘
202 { source := {z : Icc x y | z.val < y},
id ┴ └─┘ ┴ ┴ ┴└──┘ ┴ ┴
src ┴ └─┘ └──┘ ┴
typ ┴ └─┘ ┴ ┴ ┴└──┘ ┴ ┴
doc └─┘
203 target := {z : euclidean_half_space 1 | z.val 0 < y - x},
id ┴ └──────────────────┘ ┴└──┘ ┴ ┴ ┴ ┴
src ┴ └──────────────────┘ └──┘ ┴ ┴
typ ┴ └──────────────────┘ ┴└──┘ ┴ ┴ ┴ ┴
doc └──────────────────┘
204 to_fun := λ(z : Icc x y), ⟨λi, z.val - x, sub_nonneg.mpr z.property.1⟩,
id └─┘ ┴ ┴ ┴ ┴└──┘ ┴ ┴ └────────┘└──┘ ┴└───────┘┴
src └─┘ └──┘ ┴ └────────┘└──┘ └───────┘┴
typ └─┘ ┴ ┴ ┴ ┴└──┘ ┴ ┴ └────────┘└──┘ ┴└───────┘┴
doc └─┘
205 inv_fun := λz, ⟨min (z.val 0 + x) y, by simp [le_refl, z.property, le_of_lt h]⟩,
id ┴ └─┘ ┴└──┘ ┴ ┴ ┴ └─────┘ └──────┘ ┴
src └─┘ └──┘ ┴ └────┘└─────┘└┘ └┘└──────┘┴ ┴
typ ┴ └─┘ ┴└──┘ ┴ ┴ ┴ └────┘└─────┘└┘└────────┘└┘└──────┘┴┴┴
doc └────┘ └┘ └┘ ┴ ┴
txt └────┘ └┘ └┘ ┴ ┴
par └────┘ └┘ └┘ ┴ ┴
pid ┴┴ └┘ └┘ ┴ ┴
st └─────────────────────────────────────┘
206 map_source := by simp,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
207 map_target := by { simp, assume z hz, left, linarith },
src └──┘ └─────────┘ └──┘ └───────┘
typ └──┘ └─────────┘ └──┘ └───────┘
doc └──┘ └─────────┘ └──┘ └───────┘
txt └──┘ └─────────┘ └──┘ └───────┘
par └──┘ └─────────┘ └──┘ └───────┘
pid └─────────┘ ┴
st └─────┘└───────────┘└────┘└─────────┘└┘
208 left_inv := by { rintros ⟨z, hz⟩ h'z, simp at hz h'z, simp [hz, h'z] },
id └┘ └─┘
src └─────────────────┘ └────────────┘ └────┘ └┘ └┘
typ └─────────────────┘ └────────────┘ └────┘└┘└┘└─┘└┘
doc └─────────────────┘ └────────────┘ └────┘ └┘ └┘
txt └─────────────────┘ └────────────┘ └────┘ └┘ └┘
par └─────────────────┘ └────────────┘ └────┘ └┘ └┘
pid └──────────┘ ┴└───────┘ ┴┴ └┘ ┴┴
st └────────────────────┘└──────────────┘└───────────────┘└┘
209 right_inv := begin
st └─────
210 rintros ⟨z, hz⟩ h'z,
src └─────────────────┘
typ └─────────────────┘
doc └─────────────────┘
txt └─────────────────┘
par └─────────────────┘
pid └──────────┘
st ──────────────────────┘└─
211 rw subtype.mk_eq_mk,
id └──────────────┘
src └─┘└──────────────┘
typ └─┘└──────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────────────────┘└─
212 funext,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
st ─────────┘└─
213 simp at hz h'z,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴└───────┘
st ─────────────────┘└─
214 have A : x + z 0 ≤ y, by linarith,
id ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴ └─┘┴┴ └──────┘
typ └───────┘┴┴ ┴┴└─┘┴┴┴ └──────┘
doc └───────┘ ┴ ┴ └─┘ ┴ └──────┘
txt └───────┘ ┴ ┴ └─┘ ┴ └──────┘
par └───────┘ ┴ ┴ └─┘ ┴ └──────┘
pid └────┘└─┘ ┴ ┴ └─┘ ┴
st ───────────────────────┘ └─
215 rw subsingleton.elim i 0,
id └───────────────┘ ┴
src └─┘└───────────────┘┴ └┘
typ └─┘└───────────────┘┴┴└┘
doc └─┘ ┴ └┘
txt └─┘ ┴ └┘
par └─┘ ┴ └┘
pid ┴ ┴ ┴┴
st ──────────────────────────────
216 simp [A],
id ┴
src └────┘ ┴
typ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ───────────┘└─
217 end,
st ────┘
218 open_source := begin
st └─────
219 have : is_open {z : ℝ | z < y} := is_open_Iio,
id └─────┘ ┴ ┴ └─────────┘
src └─────┘└─────┘┴┴└──┘ └─┘ ┴ ┴ └───┘└─────────┘
typ └─────┘└─────┘┴┴└──┘ └─┘ ┴ ┴┴└───┘└─────────┘
doc └─────┘└─────┘┴ └──┘ └─┘ ┴ ┴ └───┘
txt └─────┘ ┴ └──┘ └─┘ ┴ ┴ └───┘
par └─────┘ ┴ └──┘ └─┘ ┴ ┴ └───┘
pid └───┘└┘ ┴ └──┘ └─┘ ┴ ┴ ┴└──┘
st ────────────────────────────────────────────────┘└─
220 exact continuous_subtype_val _ this
id └────────────────────┘ └──┘
src └────┘└────────────────────┘└─┘ └
typ └────┘└────────────────────┘└─┘└──┘└
doc └────┘ └─┘ └
txt └────┘ └─┘ └
par └────┘ └─┘ └
pid ┴ └─┘ └
st ────────────────────────────────────────
221 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
222 open_target := begin
st └─────
223 have : is_open {z : ℝ | z < y - x} := is_open_Iio,
id └─────┘ ┴ ┴ ┴ ┴ └─────────┘
src └─────┘└─────┘┴┴└──┘ └─┘ ┴ ┴ ┴┴┴ └───┘└─────────┘
typ └─────┘└─────┘┴┴└──┘ └─┘ ┴ ┴┴┴┴┴┴└───┘└─────────┘
doc └─────┘└─────┘┴ └──┘ └─┘ ┴ ┴ ┴ ┴ └───┘
txt └─────┘ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ └───┘
par └─────┘ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ └───┘
pid └───┘└┘ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴└──┘
st ────────────────────────────────────────────────────┘└─
224 have : is_open {z : fin 1 → ℝ | z 0 < y - x} :=
id └─────┘ ┴ └─┘ ┴ ┴ ┴
src └─────┘└─────┘┴┴└──┘└─┘└─┘ ┴ └─┘ └─┘ ┴ ┴ ┴ └────
typ └─────┘└─────┘┴┴└──┘└─┘└─┘┴┴ └─┘ └─┘ ┴┴┴ ┴┴└────
doc └─────┘└─────┘┴ └──┘ └─┘ ┴ └─┘ └─┘ ┴ ┴ ┴ └────
txt └─────┘ ┴ └──┘ └─┘ ┴ └─┘ └─┘ ┴ ┴ ┴ └────
par └─────┘ ┴ └──┘ └─┘ ┴ └─┘ └─┘ ┴ ┴ ┴ └────
pid └───┘└┘ ┴ └──┘ └─┘ ┴ └─┘ └─┘ ┴ ┴ ┴ ┴└───
st ────────────────────────────────────────────────────
225 (continuous_apply 0) _ this,
id └──────────────┘ └──┘
src ─────┘ └──────────────┘└────┘
typ ─────┘ └──────────────┘└────┘└──┘
doc ─────┘ └────┘
txt ─────┘ └────┘
par ─────┘ └────┘
pid ─────┘ └────┘
st ────────────────────────────────┘└─
226 exact continuous_subtype_val _ this
id └────────────────────┘ └──┘
src └────┘└────────────────────┘└─┘ └
typ └────┘└────────────────────┘└─┘└──┘└
doc └────┘ └─┘ └
txt └────┘ └─┘ └
par └────┘ └─┘ └
pid ┴ └─┘ └
st ────────────────────────────────────────
227 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
228 continuous_to_fun := begin
st └─────
229 apply continuous.continuous_on,
id └──────────────────────┘
src └────┘└──────────────────────┘
typ └────┘└──────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────────────┘└─
230 apply continuous_subtype_mk,
id └───────────────────┘
src └────┘└───────────────────┘
typ └────┘└───────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────────────┘└─
231 have : continuous (λ (z : ℝ) (i : fin 1), z - x) :=
id └────────┘ └─┘ ┴
src └─────┘└────────┘┴ └────┘ └─────┘└─┘└───┘ ┴ ┴ └────
typ └─────┘└────────┘┴ └────┘ └─────┘└─┘└───┘ ┴ ┴┴└────
doc └─────┘└────────┘┴ └────┘ └─────┘ └───┘ ┴ ┴ └────
txt └─────┘ ┴ └────┘ └─────┘ └───┘ ┴ ┴ └────
par └─────┘ ┴ └────┘ └─────┘ └───┘ ┴ ┴ └────
pid └───┘└┘ ┴ └────┘ └─────┘ └───┘ ┴ ┴ ┴└───
st ────────────────────────────────────────────────────────
232 continuous.sub (continuous_pi $ λi, continuous_id) continuous_const,
id └────────────┘ └───────────┘ └───────────┘ └──────────────┘
src ─────┘└────────────┘┴ └───────────┘┴ ┴ └─┘└───────────┘└┘└──────────────┘
typ ─────┘└────────────┘┴ └───────────┘┴ ┴ └─┘└───────────┘└┘└──────────────┘
doc ─────┘ ┴ ┴ ┴ └─┘ └┘
txt ─────┘ ┴ ┴ ┴ └─┘ └┘
par ─────┘ ┴ ┴ ┴ └─┘ └┘
pid ─────┘ ┴ ┴ ┴ └─┘ └┘
st ────────────────────────────────────────────────────────────────────────┘└─
233 exact this.comp continuous_subtype_val,
id └───────┘ └────────────────────┘
src └────┘└───────┘┴└────────────────────┘
typ └────┘└───────┘┴└────────────────────┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────────────────────────────┘└─
234 end,
st ────┘
235 continuous_inv_fun := begin
st └─────
236 apply continuous.continuous_on,
id └──────────────────────┘
src └────┘└──────────────────────┘
typ └────┘└──────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────────────┘└─
237 apply continuous_subtype_mk,
id └───────────────────┘
src └────┘└───────────────────┘
typ └────┘└───────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────────────┘└─
238 have A : continuous (λ z : ℝ, min (z + x) y) :=
id └────────┘ └─┘ ┴ ┴
src └───────┘└────────┘┴ └───┘ └┘└─┘┴ ┴ ┴ └┘ └────
typ └───────┘└────────┘┴ └───┘ └┘└─┘┴ ┴ ┴┴└┘┴└────
doc └───────┘└────────┘┴ └───┘ └┘ ┴ ┴ ┴ └┘ └────
txt └───────┘ ┴ └───┘ └┘ ┴ ┴ ┴ └┘ └────
par └───────┘ ┴ └───┘ └┘ ┴ ┴ ┴ └┘ └────
pid └────┘└─┘ ┴ └───┘ └┘ ┴ ┴ ┴ └┘ ┴└───
st ────────────────────────────────────────────────────
239 (continuous_id.add continuous_const).min continuous_const,
id └───────────────┘ └──────────────┘
src ─────┘ └───────────────┘┴ └────┘└──────────────┘
typ ─────┘ └───────────────┘┴ └────┘└──────────────┘
doc ─────┘ ┴ └────┘
txt ─────┘ ┴ └────┘
par ─────┘ ┴ └────┘
pid ─────┘ ┴ └────┘
st ──────────────────────────────────────────────────────────────┘└─
240 have B : continuous (λz : fin 1 → ℝ, z 0) := continuous_apply 0,
id └────────┘ └─┘ └──────────────┘
src └───────┘└────────┘┴ └──┘└─┘└─┘ ┴ └┘ └─────┘└──────────────┘└┘
typ └───────┘└────────┘┴ └──┘└─┘└─┘ ┴ └┘ └─────┘└──────────────┘└┘
doc └───────┘└────────┘┴ └──┘ └─┘ ┴ └┘ └─────┘ └┘
txt └───────┘ ┴ └──┘ └─┘ ┴ └┘ └─────┘ └┘
par └───────┘ ┴ └──┘ └─┘ ┴ └┘ └─────┘ └┘
pid └────┘└─┘ ┴ └──┘ └─┘ ┴ └┘ └─┘└──┘ ┴┴
st ──────────────────────────────────────────────────────────────────┘└─
241 exact (A.comp B).comp continuous_subtype_val
id └────┘ ┴ └────────────────────┘
src └────┘ └────┘┴ └─────┘└────────────────────┘└
typ └────┘ └────┘┴┴└─────┘└────────────────────┘└
doc └────┘ ┴ └─────┘ └
txt └────┘ ┴ └─────┘ └
par └────┘ ┴ └─────┘ └
pid ┴ ┴ └─────┘ └
st ─────────────────────────────────────────────────
242 end }
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
243
244 /--
245 The right chart for the topological space [x, y], defined on (x,y] and sending y to 0 in
246 `euclidean_half_space 1`.
247 -/
248 def Icc_right_chart (x y : ℝ) [h : lt_class x y] :
id ┴ └──────┘ ┴ ┴
src ┴ └──────┘
typ ┴ └──────┘ ┴ ┴
doc └──────┘
249 local_homeomorph (Icc x y) (euclidean_half_space 1) :=
id └──────────────┘ └─┘ ┴ ┴ └──────────────────┘
src └──────────────┘ └─┘ └──────────────────┘
typ └──────────────┘ └─┘ ┴ ┴ └──────────────────┘
doc └──────────────┘ └─┘ └──────────────────┘
250 { source := {z : Icc x y | x < z.val},
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴└──┘
src ┴ └─┘ ┴ └──┘
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴└──┘
doc └─┘
251 target := {z : euclidean_half_space 1 | z.val 0 < y - x},
id ┴ └──────────────────┘ ┴└──┘ ┴ ┴ ┴ ┴
src ┴ └──────────────────┘ └──┘ ┴ ┴
typ ┴ └──────────────────┘ ┴└──┘ ┴ ┴ ┴ ┴
doc └──────────────────┘
252 to_fun := λ(z : Icc x y), ⟨λi, y - z.val, sub_nonneg.mpr z.property.2⟩,
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ └────────┘└──┘ ┴└───────┘┴
src └─┘ ┴ └──┘ └────────┘└──┘ └───────┘┴
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ └────────┘└──┘ ┴└───────┘┴
doc └─┘
253 inv_fun := λz, ⟨max (y - z.val 0) x, by simp [le_refl, z.property, le_of_lt h]⟩,
id ┴ └─┘ ┴ ┴ ┴└──┘ ┴ └─────┘ └──────┘ ┴
src └─┘ ┴ └──┘ └────┘└─────┘└┘ └┘└──────┘┴ ┴
typ ┴ └─┘ ┴ ┴ ┴└──┘ ┴ └────┘└─────┘└┘└────────┘└┘└──────┘┴┴┴
doc └────┘ └┘ └┘ ┴ ┴
txt └────┘ └┘ └┘ ┴ ┴
par └────┘ └┘ └┘ ┴ ┴
pid ┴┴ └┘ └┘ ┴ ┴
st └─────────────────────────────────────┘
254 map_source := by simp,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
255 map_target := by { simp, assume z hz, left, linarith },
src └──┘ └─────────┘ └──┘ └───────┘
typ └──┘ └─────────┘ └──┘ └───────┘
doc └──┘ └─────────┘ └──┘ └───────┘
txt └──┘ └─────────┘ └──┘ └───────┘
par └──┘ └─────────┘ └──┘ └───────┘
pid └─────────┘ ┴
st └─────┘└───────────┘└────┘└─────────┘└┘
256 left_inv := by { rintros ⟨z, hz⟩ h'z, simp at hz h'z, simp [hz, h'z] },
id └┘ └─┘
src └─────────────────┘ └────────────┘ └────┘ └┘ └┘
typ └─────────────────┘ └────────────┘ └────┘└┘└┘└─┘└┘
doc └─────────────────┘ └────────────┘ └────┘ └┘ └┘
txt └─────────────────┘ └────────────┘ └────┘ └┘ └┘
par └─────────────────┘ └────────────┘ └────┘ └┘ └┘
pid └──────────┘ ┴└───────┘ ┴┴ └┘ ┴┴
st └────────────────────┘└──────────────┘└───────────────┘└┘
257 right_inv := begin
st └─────
258 rintros ⟨z, hz⟩ h'z,
src └─────────────────┘
typ └─────────────────┘
doc └─────────────────┘
txt └─────────────────┘
par └─────────────────┘
pid └──────────┘
st ──────────────────────┘└─
259 rw subtype.mk_eq_mk,
id └──────────────┘
src └─┘└──────────────┘
typ └─┘└──────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────────────────┘└─
260 funext,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
st ─────────┘└─
261 simp at hz h'z,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴└───────┘
st ─────────────────┘└─
262 have A : x ≤ y + -z 0, by linarith,
id ┴ ┴ ┴ ┴
src └───────┘ ┴┴┴ ┴ ┴ └┘ └──────┘
typ └───────┘┴┴┴┴┴┴ ┴ ┴└┘ └──────┘
doc └───────┘ ┴ ┴ ┴ ┴ └┘ └──────┘
txt └───────┘ ┴ ┴ ┴ ┴ └┘ └──────┘
par └───────┘ ┴ ┴ ┴ ┴ └┘ └──────┘
pid └────┘└─┘ ┴ ┴ ┴ ┴ ┴┴
st ────────────────────────┘ └─
263 rw subsingleton.elim i 0,
id └───────────────┘ ┴
src └─┘└───────────────┘┴ └┘
typ └─┘└───────────────┘┴┴└┘
doc └─┘ ┴ └┘
txt └─┘ ┴ └┘
par └─┘ ┴ └┘
pid ┴ ┴ ┴┴
st ──────────────────────────────
264 simp [A],
id ┴
src └────┘ ┴
typ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ───────────┘└─
265 end,
st ────┘
266 open_source := begin
st └─────
267 have : is_open {z : ℝ | x < z} := is_open_Ioi,
id └─────┘ ┴ ┴ └─────────┘
src └─────┘└─────┘┴┴└──┘ └─┘ ┴ ┴ └───┘└─────────┘
typ └─────┘└─────┘┴┴└──┘ └─┘┴┴ ┴ └───┘└─────────┘
doc └─────┘└─────┘┴ └──┘ └─┘ ┴ ┴ └───┘
txt └─────┘ ┴ └──┘ └─┘ ┴ ┴ └───┘
par └─────┘ ┴ └──┘ └─┘ ┴ ┴ └───┘
pid └───┘└┘ ┴ └──┘ └─┘ ┴ ┴ ┴└──┘
st ────────────────────────────────────────────────┘└─
268 exact continuous_subtype_val _ this
id └────────────────────┘ └──┘
src └────┘└────────────────────┘└─┘ └
typ └────┘└────────────────────┘└─┘└──┘└
doc └────┘ └─┘ └
txt └────┘ └─┘ └
par └────┘ └─┘ └
pid ┴ └─┘ └
st ────────────────────────────────────────
269 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
270 open_target := begin
st └─────
271 have : is_open {z : ℝ | z < y - x} := is_open_Iio,
id └─────┘ ┴ ┴ ┴ ┴ └─────────┘
src └─────┘└─────┘┴┴└──┘ └─┘ ┴ ┴ ┴┴┴ └───┘└─────────┘
typ └─────┘└─────┘┴┴└──┘ └─┘ ┴ ┴┴┴┴┴┴└───┘└─────────┘
doc └─────┘└─────┘┴ └──┘ └─┘ ┴ ┴ ┴ ┴ └───┘
txt └─────┘ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ └───┘
par └─────┘ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ └───┘
pid └───┘└┘ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴└──┘
st ────────────────────────────────────────────────────┘└─
272 have : is_open {z : fin 1 → ℝ | z 0 < y - x} :=
id └─────┘ ┴ └─┘ ┴ ┴ ┴
src └─────┘└─────┘┴┴└──┘└─┘└─┘ ┴ └─┘ └─┘ ┴ ┴ ┴ └────
typ └─────┘└─────┘┴┴└──┘└─┘└─┘┴┴ └─┘ └─┘ ┴┴┴ ┴┴└────
doc └─────┘└─────┘┴ └──┘ └─┘ ┴ └─┘ └─┘ ┴ ┴ ┴ └────
txt └─────┘ ┴ └──┘ └─┘ ┴ └─┘ └─┘ ┴ ┴ ┴ └────
par └─────┘ ┴ └──┘ └─┘ ┴ └─┘ └─┘ ┴ ┴ ┴ └────
pid └───┘└┘ ┴ └──┘ └─┘ ┴ └─┘ └─┘ ┴ ┴ ┴ ┴└───
st ────────────────────────────────────────────────────
273 (continuous_apply 0) _ this,
id └──────────────┘ └──┘
src ─────┘ └──────────────┘└────┘
typ ─────┘ └──────────────┘└────┘└──┘
doc ─────┘ └────┘
txt ─────┘ └────┘
par ─────┘ └────┘
pid ─────┘ └────┘
st ────────────────────────────────┘└─
274 exact continuous_subtype_val _ this
id └────────────────────┘ └──┘
src └────┘└────────────────────┘└─┘ └
typ └────┘└────────────────────┘└─┘└──┘└
doc └────┘ └─┘ └
txt └────┘ └─┘ └
par └────┘ └─┘ └
pid ┴ └─┘ └
st ────────────────────────────────────────
275 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
276 continuous_to_fun := begin
277 apply continuous.continuous_on,
278 apply continuous_subtype_mk,
st └─
279 have : continuous (λ (z : ℝ) (i : fin 1), y - z) :=
id └────────┘ └─┘ ┴
src └─────┘└────────┘┴ └────┘ └─────┘└─┘└───┘ ┴ ┴ └────
typ └─────┘└────────┘┴ └────┘ └─────┘└─┘└───┘┴┴ ┴ └────
doc └─────┘└────────┘┴ └────┘ └─────┘ └───┘ ┴ ┴ └────
txt └─────┘ ┴ └────┘ └─────┘ └───┘ ┴ ┴ └────
par └─────┘ ┴ └────┘ └─────┘ └───┘ ┴ ┴ └────
pid └───┘└┘ ┴ └────┘ └─────┘ └───┘ ┴ ┴ ┴└───
st ────────────────────────────────────────────────────────
280 continuous_const.sub (continuous_pi (λi, continuous_id)),
id └──────────────────┘ └───────────┘ └───────────┘
src ─────┘└──────────────────┘┴ └───────────┘┴ └─┘└───────────┘└┘
typ ─────┘└──────────────────┘┴ └───────────┘┴ └─┘└───────────┘└┘
doc ─────┘ ┴ ┴ └─┘ └┘
txt ─────┘ ┴ ┴ └─┘ └┘
par ─────┘ ┴ ┴ └─┘ └┘
pid ─────┘ ┴ ┴ └─┘ └┘
st ─────────────────────────────────────────────────────────────┘└─
281 exact this.comp continuous_subtype_val,
id └───────┘ └────────────────────┘
src └────┘└───────┘┴└────────────────────┘
typ └────┘└───────┘┴└────────────────────┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────────────────────────────┘└─
282 end,
st ────┘
283 continuous_inv_fun := begin
284 apply continuous.continuous_on,
285 apply continuous_subtype_mk,
st └─
286 have A : continuous (λ z : ℝ, max (y - z) x) :=
id └────────┘ └─┘ ┴ ┴
src └───────┘└────────┘┴ └───┘ └┘└─┘┴ ┴ ┴ └┘ └────
typ └───────┘└────────┘┴ └───┘ └┘└─┘┴ ┴┴ ┴ └┘┴└────
doc └───────┘└────────┘┴ └───┘ └┘ ┴ ┴ ┴ └┘ └────
txt └───────┘ ┴ └───┘ └┘ ┴ ┴ ┴ └┘ └────
par └───────┘ ┴ └───┘ └┘ ┴ ┴ ┴ └┘ └────
pid └────┘└─┘ ┴ └───┘ └┘ ┴ ┴ ┴ └┘ ┴└───
st ────────────────────────────────────────────────────
287 (continuous_const.sub continuous_id).max continuous_const,
id └──────────────────┘ └───────────┘ └──────────────┘
src ─────┘ └──────────────────┘┴└───────────┘└────┘└──────────────┘
typ ─────┘ └──────────────────┘┴└───────────┘└────┘└──────────────┘
doc ─────┘ ┴ └────┘
txt ─────┘ ┴ └────┘
par ─────┘ ┴ └────┘
pid ─────┘ ┴ └────┘
st ──────────────────────────────────────────────────────────────┘└─
288 have B : continuous (λz : fin 1 → ℝ, z 0) := continuous_apply 0,
id └────────┘ └─┘ └──────────────┘
src └───────┘└────────┘┴ └──┘└─┘└─┘ ┴ └┘ └─────┘└──────────────┘└┘
typ └───────┘└────────┘┴ └──┘└─┘└─┘ ┴ └┘ └─────┘└──────────────┘└┘
doc └───────┘└────────┘┴ └──┘ └─┘ ┴ └┘ └─────┘ └┘
txt └───────┘ ┴ └──┘ └─┘ ┴ └┘ └─────┘ └┘
par └───────┘ ┴ └──┘ └─┘ ┴ └┘ └─────┘ └┘
pid └────┘└─┘ ┴ └──┘ └─┘ ┴ └┘ └─┘└──┘ ┴┴
st ──────────────────────────────────────────────────────────────────┘└─
289 exact (A.comp B).comp continuous_subtype_val
id └────┘ ┴ └────────────────────┘
src └────┘ └────┘┴ └─────┘└────────────────────┘└
typ └────┘ └────┘┴┴└─────┘└────────────────────┘└
doc └────┘ ┴ └─────┘ └
txt └────┘ ┴ └─────┘ └
par └────┘ ┴ └─────┘ └
pid ┴ ┴ └─────┘ └
st ─────────────────────────────────────────────────
290 end }
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
291
292 /--
293 Manifold with boundary structure on [x, y], using only two charts.
294 -/
295 instance Icc_manifold (x y : ℝ) [h : lt_class x y] : manifold (euclidean_half_space 1) (Icc x y) :=
id ┴ └──────┘ ┴ ┴ └──────┘ └──────────────────┘ └─┘ ┴ ┴
src ┴ └──────┘ └──────┘ └──────────────────┘ └─┘
typ ┴ └──────┘ ┴ ┴ └──────┘ └──────────────────┘ └─┘ ┴ ┴
doc └──────┘ └──────┘ └──────────────────┘ └─┘
296 { atlas := {Icc_left_chart x y, Icc_right_chart x y},
id ┴└────────────┘ ┴ ┴┴ └─────────────┘ ┴ ┴
src ┴└────────────┘ ┴ └─────────────┘
typ ┴└────────────┘ ┴ ┴┴ └─────────────┘ ┴ ┴
doc └────────────┘ └─────────────┘
297 chart_at := λz, if z.val < y then Icc_left_chart x y else Icc_right_chart x y,
id ┴ ┴└──┘ ┴ ┴ └────────────┘ ┴ ┴ └─────────────┘ ┴ ┴
src └──┘ ┴ └────────────┘ └─────────────┘
typ ┴ ┴└──┘ ┴ ┴ └────────────┘ ┴ ┴ └─────────────┘ ┴ ┴
doc └────────────┘ └─────────────┘
298 mem_chart_source := λz, begin
id ┴
typ ┴
st └─────
299 by_cases h' : z.val < y,
id └───┘ ┴ ┴
src └───────┘ └─┘└───┘┴┴┴
typ └───────┘ └─┘└───┘┴┴┴┴
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ──────────────────────────┘└─
300 { simp only [h', if_true],
id └┘ └─────┘
src └─────────┘ └┘└─────┘┴
typ └─────────┘└┘└┘└─────┘┴
doc └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st ─────┘└─────────────────────┘└─
301 exact h' },
id └┘
src └────┘ ┴
typ └────┘└┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────┘└┘└
302 { simp only [h', if_false],
id └┘ └──────┘
src └─────────┘ └┘└──────┘┴
typ └─────────┘└┘└┘└──────┘┴
doc └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st ─────────────────────────────┘└─
303 apply lt_of_lt_of_le h,
id └────────────┘ ┴
src └────┘└────────────┘┴
typ └────┘└────────────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────────┘└─
304 simpa using h' }
id └┘
src └──────────┘ ┴
typ └──────────┘└┘┴
doc └──────────┘ ┴
txt └──────────┘ ┴
par └──────────┘ ┴
pid ┴└────┘ ┴
st ────────────────────┘└─
305 end,
st ────┘
306 chart_mem_atlas := λz, by { by_cases h' : z.val < y; simp [h'] } }
id ┴ └───┘ ┴ └┘
src └───────┘ └─┘└───┘┴ ┴ └────┘ └┘
typ ┴ └───────┘ └─┘└───┘┴ ┴┴ └────┘└┘└┘
doc └───────┘ └─┘ ┴ ┴ └────┘ └┘
txt └───────┘ └─┘ ┴ ┴ └────┘ └┘
par └───────┘ └─┘ ┴ ┴ └────┘ └┘
pid ┴ └─┘ ┴ ┴ ┴┴ ┴┴
st └────────────────────────────────────┘└┘
307
308 /--
309 The manifold structure on [x, y] is smooth.
310 -/
311 instance Icc_smooth_manifold (x y : ℝ) [lt_class x y] :
id ┴ └──────┘ ┴ ┴
src ┴ └──────┘
typ ┴ └──────┘ ┴ ┴
doc └──────┘
312 smooth_manifold_with_corners (model_with_corners_euclidean_half_space 1) (Icc x y) :=
id └──────────────────────────┘ └─────────────────────────────────────┘ └─┘ ┴ ┴
src └──────────────────────────┘ └─────────────────────────────────────┘ └─┘
typ └──────────────────────────┘ └─────────────────────────────────────┘ └─┘ ┴ ┴
doc └──────────────────────────┘ └─────────────────────────────────────┘ └─┘
313 begin
st └─────
314 have M : times_cont_diff_on ℝ ⊤ (λz : fin 1 → ℝ, (λi : fin 1, y - x) - z) univ,
id └────────────────┘ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ └──┘
src └───────┘└────────────────┘┴ ┴┴┴ └──┘ └─┘ ┴ └┘ └──┘└─┘└──┘ ┴┴┴ └┘ ┴ └┘└──┘
typ └───────┘└────────────────┘┴ ┴┴┴ └──┘└─┘└─┘┴┴ └┘ └──┘└─┘└──┘┴┴┴┴┴└┘ ┴ └┘└──┘
doc └───────┘└────────────────┘┴ ┴ ┴ └──┘ └─┘ ┴ └┘ └──┘ └──┘ ┴ ┴ └┘ ┴ └┘
txt └───────┘ ┴ ┴ ┴ └──┘ └─┘ ┴ └┘ └──┘ └──┘ ┴ ┴ └┘ ┴ └┘
par └───────┘ ┴ ┴ ┴ └──┘ └─┘ ┴ └┘ └──┘ └──┘ ┴ ┴ └┘ ┴ └┘
pid └────┘└─┘ ┴ ┴ ┴ └──┘ └─┘ ┴ └┘ └──┘ └──┘ ┴ ┴ └┘ ┴ └┘
st ───────────────────────────────────────────────────────────────────────────────┘└┘
315 { rw times_cont_diff_on_univ,
316 exact times_cont_diff.sub times_cont_diff_const times_cont_diff_id },
st └┘
317 haveI : has_groupoid (Icc x y)
id ┴ ┴
typ ┴ ┴
318 (times_cont_diff_groupoid ⊤ (model_with_corners_euclidean_half_space 1)) :=
319 begin
320 apply has_groupoid_of_pregroupoid,
321 assume e e' he he',
322 simp [atlas] at he he',
323 /- We need to check that any composition of two charts gives a C^∞ function. Each chart can be
324 either the left chart or the right chart, leaving 4 possibilities that we handle successively.
325 -/
326 rcases he with rfl | rfl; rcases he' with rfl | rfl,
327 { -- e = right chart, e' = right chart
328 refine ((mem_groupoid_of_pregroupoid _ _).mpr _).1,
329 exact symm_trans_mem_times_cont_diff_groupoid _ _ _ },
st └┘
330 { -- e = right chart, e' = left chart
331 apply M.congr_mono _ _ (subset_univ _),
332 { rw inter_comm,
333 refine unique_diff_on.inter (model_with_corners.unique_diff _) _,
334 exact model_with_corners.continuous_inv_fun _ _ (local_homeomorph.open_source _) },
st └┘
335 { assume z hz,
336 simp [-mem_range, range_half_space, model_with_corners_euclidean_half_space,
337 local_equiv.trans_source, Icc_left_chart, Icc_right_chart] at hz,
338 have A : 0 ≤ z 0 := hz.2,
id ┴
typ ┴
339 have B : x ≤ y + -z 0, by { have := hz.1.1.1, linarith },
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └┘
340 have C : y + (-x + -z 0) = ((λ (i : fin 1), y + -x) + -z) 0,
id └─┘ ┴ ┴
src └─┘
typ └─┘ ┴ ┴
341 by { change y + (-x - z 0) = (y - x) - z 0, ring },
id ┴ ┴
typ ┴ ┴
st └┘
342 ext i,
343 rw subsingleton.elim i 0,
id ┴
typ ┴
344 simpa [model_with_corners_euclidean_half_space, Icc_left_chart, Icc_right_chart, A, B] } },
st └──┘
345 { -- e = left chart, e' = right chart
346 apply M.congr_mono _ _ (subset_univ _),
347 { rw inter_comm,
348 refine unique_diff_on.inter (model_with_corners.unique_diff _) _,
349 exact model_with_corners.continuous_inv_fun _ _ (local_homeomorph.open_source _) },
st └┘
350 { assume z hz,
351 simp [-mem_range, range_half_space, model_with_corners_euclidean_half_space,
352 local_equiv.trans_source, Icc_left_chart, Icc_right_chart] at hz,
353 have A : 0 ≤ z 0 := hz.2,
id ┴
typ ┴
354 have B : x + z 0 ≤ y, by { have := hz.1.1.1, linarith },
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └┘
355 have C : y + (-x + -z 0) = ((λ (i : fin 1), y + -x) + -z) 0,
id └─┘ ┴ ┴
src └─┘
typ └─┘ ┴ ┴
356 by { change y + (-x - z 0) = (y - x) - z 0, ring },
id ┴ ┴
typ ┴ ┴
st └┘
357 ext i,
358 rw subsingleton.elim i 0,
id ┴
typ ┴
359 simpa [model_with_corners_euclidean_half_space, Icc_left_chart, Icc_right_chart, A, B] } },
st └──┘
360 { -- e = left chart, e' = left chart
361 refine ((mem_groupoid_of_pregroupoid _ _).mpr _).1,
362 exact symm_trans_mem_times_cont_diff_groupoid _ _ _ }
st └┘
363 end,
st └─┘
364 constructor
365 end
st └─┘